$\forall$${\it es}$:ES, $p$:(E$\rightarrow$(E + Top)).
\\[0ex]causal{-}predecessor(${\it es}$;$p$) $\Rightarrow$ ($\forall$$e$, ${\it e'}$:E. Dec(same{-}thread(${\it es}$;$p$;$e$;${\it e'}$)))